FDL - Nuprl Definition : existse-between2

Nuprl Definition : existse-between2

0,22

[e1,e2].P(e) ==

e:E. e1

e & e

e2 & P(e)

clarification:

existse-between2(es;e1;e2;e.P(e)) ==

e:es-E(es). es-le(es;e1;e) & es-le(es;e;e2) & P(e)

Definitions x:A. B(x), E, A & B, P & Q, e e'

FDL editor aliases existse-between2

Definitions	x:A. B(x), E, A & B, P & Q, e e'
FDL editor aliases	existse-between2